1 /-
2 Copyright (c) 2019 Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Chris Hughes
5 -/
6
7 import ring_theory.noetherian linear_algebra.dimension
src └────────────────────┘ └──────────────────────┘
8 import ring_theory.principal_ideal_domain
src └────────────────────────────────┘
9
10 /-!
11 # Finite dimensional vector spaces
12
13 Definition and basic properties of finite dimensional vector spaces, of their dimensions, and
14 of linear maps on such spaces.
15
16 ## Main definitions
17
18 Assume `V` is a vector space over a field `K`. There are (at least) three equivalent definitions of
19 finite-dimensionality of `V`:
20
21 - it admits a finite basis.
22 - it is finitely generated.
23 - it is noetherian, i.e., every subspace is finitely generated.
24
25 We introduce a typeclass `finite_dimensional K V` capturing this property. For ease of transfer of
26 proof, it is defined using the third point of view, i.e., as `is_noetherian`. However, we prove
27 that all these points of view are equivalent, with the following lemmas
28 (in the namespace `finite_dimensional`):
29
30 - `exists_is_basis_finite` states that a finite-dimensional vector space has a finite basis
31 - `of_finite_basis` states that the existence of a finite basis implies finite-dimensionality
32 - `iff_fg` states that the space is finite-dimensional if and only if it is finitely generated
33
34 Also defined is `findim`, the dimension of a finite dimensional space, returning a `nat`,
35 as opposed to `dim`, which returns a `cardinal`. When the space has infinite dimension, its
36 `findim` is by convention set to `0`.
37
38 Preservation of finite-dimensionality and formulas for the dimension are given for
39 - submodules
40 - quotients (for the dimension of a quotient, see `findim_quotient_add_findim`)
41 - linear equivs, in `linear_equiv.finite_dimensional` and `linear_equiv.findim_eq`
42 - image under a linear map (the rank-nullity formula is in `findim_range_add_findim_ker`)
43
44 Basic properties of linear maps of a finite-dimensional vector space are given. Notably, the
45 equivalence of injectivity and surjectivity is proved in `linear_map.injective_iff_surjective`,
46 and the equivalence between left-inverse and right-inverse in `mul_eq_one_comm` and
47 `comp_eq_id_comm`.
48
49 ## Implementation notes
50
51 Most results are deduced from the corresponding results for the general dimension (as a cardinal),
52 in `dimension.lean`. Not all results have been ported yet.
53
54 One of the characterizations of finite-dimensionality is in terms of finite generation. This
55 property is currently defined only for submodules, so we express it through the fact that the
56 maximal submodule (which, as a set, coincides with the whole space) is finitely generated. This is
57 not very convenient to use, although there are some helper functions. However, this becomes very
58 convenient when speaking of submodules which are finite-dimensional, as this notion coincides with
59 the fact that the submodule is finitely generated (as a submodule of the whole space). This
60 equivalence is proved in `submodule.fg_iff_finite_dimensional`.
61 -/
62
63 universes u v v' w
64 open_locale classical
65
66 open vector_space cardinal submodule module function
67
68 variables {K : Type u} {V : Type v} [discrete_field K] [add_comm_group V] [vector_space K V]
id └────────────┘ └────────────┘ └──────────┘
src └────────────┘ └────────────┘ └──────────┘
typ └────────────┘ └────────────┘ └──────────┘
doc └──────────┘
69 {V₂ : Type v'} [add_comm_group V₂] [vector_space K V₂]
id └────────────┘ └──────────┘
src └────────────┘ └──────────┘
typ └────────────┘ └──────────┘
doc └──────────┘
70
71 /-- `finite_dimensional` vector spaces are defined to be noetherian modules.
72 Use `finite_dimensional.iff_fg` or `finite_dimensional.of_finite_basis` to prove finite dimension
73 from a conventional definition. -/
74 @[reducible] def finite_dimensional (K V : Type*) [discrete_field K]
id └────────────┘ ┴
src └────────────┘
typ └────────────┘ ┴
doc └───────┘
75 [add_comm_group V] [vector_space K V] := is_noetherian K V
id └────────────┘ ┴ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └────────────┘ └──────────┘ └───────────┘
typ └────────────┘ ┴ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └──────────┘
76
77 namespace finite_dimensional
78
79 open is_noetherian
80
81 /-- A vector space is finite-dimensional if and only if its dimension (as a cardinal) is strictly
82 less than the first infinite cardinal `omega`. -/
83 lemma finite_dimensional_iff_dim_lt_omega : finite_dimensional K V ↔ dim K V < omega.{v} :=
id └────────────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───┘
src └────────────────┘ ┴ └─┘ ┴ └───┘
typ └────────────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───┘
doc └────────────────┘ └───┘
84 begin
st └─────
85 cases exists_is_basis K V with b hb,
id └─────────────┘ ┴ ┴
src └────┘└─────────────┘┴ ┴ └────────┘
typ └────┘└─────────────┘┴┴┴┴└────────┘
doc └────┘ ┴ ┴ └────────┘
txt └────┘ ┴ ┴ └────────┘
par └────┘ ┴ ┴ └────────┘
pid ┴ ┴ ┴ └────────┘
st ────────────────────────────────────┘└─
86 have := is_basis.mk_eq_dim hb,
id └────────────────┘ └┘
src └──────┘└────────────────┘┴
typ └──────┘└────────────────┘┴└┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ──────────────────────────────┘└─
87 simp only [lift_id] at this,
id └─────┘
src └─────────┘└─────┘└───────┘
typ └─────────┘└─────┘└───────┘
doc └─────────┘ └───────┘
txt └─────────┘ └───────┘
par └─────────┘ └───────┘
pid ┴└──┘└┘ ┴┴└─────┘
st ────────────────────────────┘└─
88 rw [← this, lt_omega_iff_fintype, ← @set.set_of_mem_eq _ b, ← subtype.val_range],
id └──┘ └──────────────────┘ └───────────────┘ ┴ └───────────────┘
src └────┘ └┘└──────────────────┘└──┘ └───────────────┘└─┘ └──┘└───────────────┘┴
typ └────┘└──┘└┘└──────────────────┘└──┘ └───────────────┘└─┘┴└──┘└───────────────┘┴
doc └────┘ └┘ └──┘ └─┘ └──┘ ┴
txt └────┘ └┘ └──┘ └─┘ └──┘ ┴
par └────┘ └┘ └──┘ └─┘ └──┘ ┴
pid └──┘ └┘ └──┘ └─┘ └──┘ ┴
st ───────────┘└────────────────────┘└────────────────────────┘└───────────────────┘└──
89 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
90 { intro, resetI, convert finite_of_linear_independent hb.1, simp },
id └──────────────────────────┘ └┘
src └───┘ └────┘ └──────┘└──────────────────────────┘┴ └┘ └───┘
typ └───┘ └────┘ └──────┘└──────────────────────────┘┴└┘└┘ └───┘
doc └───┘ └────┘ └──────┘ ┴ └┘ └───┘
txt └───┘ └────┘ └──────┘ ┴ └┘ └───┘
par └───┘ └────┘ └──────┘ ┴ └┘ └───┘
pid ┴ ┴ └┘ ┴
st ───┘└───┘└─────────────────────────────────────────────────┘└─────┘└┘└
91 { assume hbfinite,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └─────────────┘
st ──────────────────┘└─
92 refine @is_noetherian_of_linear_equiv K (⊤ : submodule K V) V _
id └───────────────────────────┘ ┴ └───────┘ ┴ ┴
src └─────┘ └───────────────────────────┘┴ ┴ ┴└─┘└───────┘┴ ┴ └┘ └──
typ └─────┘ └───────────────────────────┘┴ ┴ ┴└─┘└───────┘┴┴┴ └┘┴└──
doc └─────┘ ┴ ┴ └─┘└───────┘┴ ┴ └┘ └──
txt └─────┘ ┴ ┴ └─┘ ┴ ┴ └┘ └──
par └─────┘ ┴ ┴ └─┘ ┴ ┴ └┘ └──
pid ┴ ┴ ┴ └─┘ ┴ ┴ └┘ └──
st ────────────────────────────────────────────────────────────────────
93 _ _ _ _ (linear_equiv.of_top _ rfl) (id _),
id └─────────────────┘ └─┘ └┘
src ─────────────┘ └─────────────────┘└─┘└─┘└┘ └┘└─┘
typ ─────────────┘ └─────────────────┘└─┘└─┘└┘ └┘└─┘
doc ─────────────┘ └─────────────────┘└─┘ └┘ └─┘
txt ─────────────┘ └─┘ └┘ └─┘
par ─────────────┘ └─┘ └┘ └─┘
pid ─────────────┘ └─┘ └┘ └─┘
st ───────────────────────────────────────────────┘└─
94 refine is_noetherian_of_fg_of_noetherian _ ⟨set.finite.to_finset hbfinite, _⟩,
id └───────────────────────────────┘ └──────────────────┘ └──────┘
src └─────┘└───────────────────────────────┘└─┘ └──────────────────┘┴ └──┘
typ └─────┘└───────────────────────────────┘└─┘ └──────────────────┘┴└──────┘└──┘
doc └─────┘ └─┘ └──────────────────┘┴ └──┘
txt └─────┘ └─┘ ┴ └──┘
par └─────┘ └─┘ ┴ └──┘
pid ┴ └─┘ ┴ └──┘
st ────────────────────────────────────────────────────────────────────────────────┘└─
95 rw [set.finite.coe_to_finset, ← hb.2], refl }
id └──────────────────────┘ └┘
src └──┘└──────────────────────┘└──┘ └─┘ └───┘
typ └──┘└──────────────────────┘└──┘└┘└─┘ └───┘
doc └──┘ └──┘ └─┘ └───┘
txt └──┘ └──┘ └─┘ └───┘
par └──┘ └──┘ └─┘ └───┘
pid └┘ └──┘ └─┘ ┴
st ───────────────────────────────┘└────┘└────────┘└─
96 end
st ──┘
97
98 /-- The dimension of a finite-dimensional vector space, as a cardinal, is strictly less than the
99 first infinite cardinal `omega`. -/
100 lemma dim_lt_omega (K V : Type*) [discrete_field K] [add_comm_group V] [vector_space K V] :
id └────────────┘ ┴ └────────────┘ ┴ └──────────┘ ┴ ┴
src └────────────┘ └────────────┘ └──────────┘
typ └────────────┘ ┴ └────────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘
101 ∀ [finite_dimensional K V], dim K V < omega.{v} :=
id └────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───┘
src └────────────────┘ └─┘ ┴ └───┘
typ └────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───┘
doc └────────────────┘ └───┘
102 finite_dimensional_iff_dim_lt_omega.1
id └─────────────────────────────────┘┴
src └─────────────────────────────────┘┴
typ └─────────────────────────────────┘┴
doc └─────────────────────────────────┘
103
104 /-- In a finite dimensional space, there exists a finite basis. A basis is in general given as a
st ┴
105 function from an arbitrary type to the vector space. Here, we think of a basis as a set (instead of
st ┴
106 a function), and use as parametrizing type this set (and as a function the function `subtype.val`).
107 -/
108 variables (K V)
109 lemma exists_is_basis_finite [finite_dimensional K V] :
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
doc └────────────────┘
110 ∃ s : set V, (is_basis K (subtype.val : s → V)) ∧ s.finite :=
id ┴ └─┘ ┴┴ └──────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴└─────┘
src ┴ └─┘ ┴ └──────┘ └─────────┘ ┴ └─────┘
typ ┴ └─┘ ┴┴ └──────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴└─────┘
doc └──────┘ └─────┘
111 begin
st └─────
112 cases exists_is_basis K V with s hs,
id └─────────────┘ ┴ ┴
src └────┘└─────────────┘┴ ┴ └────────┘
typ └────┘└─────────────┘┴┴┴┴└────────┘
doc └────┘ ┴ ┴ └────────┘
txt └────┘ ┴ ┴ └────────┘
par └────┘ ┴ ┴ └────────┘
pid ┴ ┴ ┴ └────────┘
st ────────────────────────────────────┘└─
113 exact ⟨s, hs, finite_of_linear_independent hs.1⟩
id ┴ └──────────────────────────┘ └┘
src └────┘ └┘ └┘└──────────────────────────┘┴ └──┘
typ └────┘ ┴└┘ └┘└──────────────────────────┘┴└┘└──┘
doc └────┘ └┘ └┘ ┴ └──┘
txt └────┘ └┘ └┘ ┴ └──┘
par └────┘ └┘ └┘ ┴ └──┘
pid ┴ └┘ └┘ ┴ └─┘┴
st ──────────────────────────────────────────────────┘
114 end
st └─┘
115 variables {K V}
116
117 /-- A vector space is finite-dimensional if and only if it is finitely generated. As the
118 finitely-generated property is a property of submodules, we formulate this in terms of the
119 maximal submodule, equal to the whole space as a set by definition.-/
120 lemma iff_fg :
121 finite_dimensional K V ↔ (⊤ : submodule K V).fg :=
id └────────────────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘
src └────────────────┘ ┴ ┴ └───────┘ └┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘
doc └────────────────┘ └───────┘
122 begin
st └─────
123 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
124 { introI h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ───┘└──────┘└─
125 rcases exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
id └────────────────────┘ ┴ ┴
src └─────┘└────────────────────┘┴ ┴ └──────────────────────────┘
typ └─────┘└────────────────────┘┴┴┴┴└──────────────────────────┘
doc └─────┘ ┴ ┴ └──────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────┘
st ────────────────────────────────────────────────────────────────┘└─
126 exact ⟨s_finite.to_finset, by { convert s_basis.2, simp }⟩ },
id └────────────────┘ └─────┘
src └────┘ └────────────────┘└┘ └─┘└──────┘ └┘└┘└───┘└─┘
typ └────┘ └────────────────┘└┘ └─┘└──────┘└─────┘└┘└┘└───┘└─┘
doc └────┘ └────────────────┘└┘ └─┘└──────┘ └┘└┘└───┘└─┘
txt └────┘ └┘ └─┘└──────┘ └┘└┘└───┘└─┘
par └────┘ └┘ └─┘└──────┘ └┘└┘└───┘└─┘
pid ┴ └┘ └─────────┘ └─────────┘┴
st ────────────────────────────────┘└──────────────────┘└─────┘┴└┘└┘└
127 { rintros ⟨s, hs⟩,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └──────┘
st ──────────────────┘└─
128 rw [finite_dimensional_iff_dim_lt_omega, ← dim_top, ← hs],
id └─────────────────────────────────┘ └─────┘ └┘
src └──┘└─────────────────────────────────┘└──┘└─────┘└──┘ ┴
typ └──┘└─────────────────────────────────┘└──┘└─────┘└──┘└┘┴
doc └──┘└─────────────────────────────────┘└──┘ └──┘ ┴
txt └──┘ └──┘ └──┘ ┴
par └──┘ └──┘ └──┘ ┴
pid └┘ └──┘ └──┘ ┴
st ──────────────────────────────────────────┘└─────────┘└────┘└──
129 exact lt_of_le_of_lt (dim_span_le _) (lt_omega_iff_finite.2 (set.finite_mem_finset s)) }
id └────────────┘ └─────────┘ └─────────────────┘ └───────────────────┘ ┴
src └────┘└────────────┘┴ └─────────┘└──┘ └─────────────────┘└─┘ └───────────────────┘┴ └─┘
typ └────┘└────────────┘┴ └─────────┘└──┘ └─────────────────┘└─┘ └───────────────────┘┴┴└─┘
doc └────┘ ┴ └──┘ └─┘ ┴ └─┘
txt └────┘ ┴ └──┘ └─┘ ┴ └─┘
par └────┘ ┴ └──┘ └─┘ ┴ └─┘
pid ┴ ┴ └──┘ └─┘ ┴ └┘┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
130 end
st ──┘
131
132 /-- If a vector space has a finite basis, then it is finite-dimensional. -/
133 lemma of_finite_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :
id └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └─────┘ └──────┘
typ └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └─────┘ └──────┘
134 finite_dimensional K V :=
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
doc └────────────────┘
135 iff_fg.2 $ ⟨finset.univ.image b, by {convert h.2, simp} ⟩
id └────┘┴ └─────────┘└────┘ ┴ ┴
src └────┘┴ └─────────┘└────┘ └──────┘ └┘ └──┘
typ └────┘┴ └─────────┘└────┘ ┴ └──────┘┴└┘ └──┘
doc └────┘ └─────────┘└────┘ └──────┘ └┘ └──┘
txt └──────┘ └┘ └──┘
par └──────┘ └┘ └──┘
pid ┴ └┘
st └───────────┘└────┘└┘
136
137 /-- A subspace of a finite-dimensional space is also finite-dimensional. -/
138 instance finite_dimensional_submodule [finite_dimensional K V] (S : submodule K V) :
id └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
src └────────────────┘ └───────┘
typ └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
doc └────────────────┘ └───────┘
139 finite_dimensional K S :=
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
doc └────────────────┘
140 finite_dimensional_iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_submodule_le _) (dim_lt_omega K V))
id └─────────────────────────────────┘┴ └────────────┘ └──────────────┘ └──────────┘ ┴ ┴
src └─────────────────────────────────┘┴ └────────────┘ └──────────────┘ └──────────┘
typ └─────────────────────────────────┘┴ └────────────┘ └──────────────┘ └──────────┘ ┴ ┴
doc └─────────────────────────────────┘ └──────────┘
141
142 /-- A quotient of a finite-dimensional space is also finite-dimensional. -/
143 instance finite_dimensional_quotient [finite_dimensional K V] (S : submodule K V) :
id └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
src └────────────────┘ └───────┘
typ └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
doc └────────────────┘ └───────┘
144 finite_dimensional K (quotient S) :=
id └────────────────┘ ┴ └──────┘ ┴
src └────────────────┘ └──────┘
typ └────────────────┘ ┴ └──────┘ ┴
doc └────────────────┘ └──────┘
145 finite_dimensional_iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_quotient_le _) (dim_lt_omega K V))
id └─────────────────────────────────┘┴ └────────────┘ └─────────────┘ └──────────┘ ┴ ┴
src └─────────────────────────────────┘┴ └────────────┘ └─────────────┘ └──────────┘
typ └─────────────────────────────────┘┴ └────────────┘ └─────────────┘ └──────────┘ ┴ ┴
doc └─────────────────────────────────┘ └──────────┘
146
147 /-- The dimension of a finite-dimensional vector space as a natural number. Defined by convention to
148 be `0` if the space is infinite-dimensional. -/
149 noncomputable def findim (K V : Type*) [discrete_field K]
id └────────────┘ ┴
src └────────────┘
typ └────────────┘ ┴
150 [add_comm_group V] [vector_space K V] : ℕ :=
id └────────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └────────────┘ └──────────┘ ┴
typ └────────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
151 if h : dim K V < omega.{v} then classical.some (lt_omega.1 h) else 0
id └┘ └─┘ ┴ ┴ ┴ └───┘ └────────────┘ └──────┘┴ ┴ ┴
src └┘ └─┘ ┴ └───┘ └────────────┘ └──────┘┴ ┴
typ └┘ └─┘ ┴ ┴ ┴ └───┘ └────────────┘ └──────┘┴ ┴ ┴
doc └───┘
152
153 /-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its `findim`. -/
154 lemma findim_eq_dim (K : Type u) (V : Type v) [discrete_field K]
id └────────────┘ ┴
src └────────────┘
typ └────────────┘ ┴
155 [add_comm_group V] [vector_space K V] [finite_dimensional K V] :
id └────────────┘ ┴ └──────────┘ ┴ ┴ └────────────────┘ ┴ ┴
src └────────────┘ └──────────┘ └────────────────┘
typ └────────────┘ ┴ └──────────┘ ┴ ┴ └────────────────┘ ┴ ┴
doc └──────────┘ └────────────────┘
156 (findim K V : cardinal.{v}) = dim K V :=
id └────┘ ┴ ┴ └──────┘ ┴ └─┘ ┴ ┴
src └────┘ └──────┘ ┴ └─┘
typ └────┘ ┴ ┴ └──────┘ ┴ └─┘ ┴ ┴
doc └────┘ └──────┘
157 begin
st └─────
158 have : findim K V = classical.some (lt_omega.1 (dim_lt_omega K V)) :=
id └────┘ ┴ └────────────┘ └──────┘ └──────────┘ ┴ ┴
src └─────┘└────┘┴ ┴ ┴┴┴└────────────┘┴ └──────┘└─┘ └──────────┘┴ ┴ └─────
typ └─────┘└────┘┴ ┴ ┴┴┴└────────────┘┴ └──────┘└─┘ └──────────┘┴┴┴┴└─────
doc └─────┘└────┘┴ ┴ ┴ ┴ ┴ └─┘ └──────────┘┴ ┴ └─────
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────
par └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘└───
st ────────────────────────────────────────────────────────────────────────
159 dif_pos (dim_lt_omega K V),
id └─────┘ └──────────┘ ┴ ┴
src ───┘└─────┘┴ └──────────┘┴ ┴ ┴
typ ───┘└─────┘┴ └──────────┘┴┴┴┴┴
doc ───┘ ┴ └──────────┘┴ ┴ ┴
txt ───┘ ┴ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴ ┴
st ─────────────────────────────┘└─
160 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
161 exact (classical.some_spec (lt_omega.1 (dim_lt_omega K V))).symm
id └─────────────────┘ └──────┘ └──────────┘ ┴ ┴
src └────┘ └─────────────────┘┴ └──────┘└─┘ └──────────┘┴ ┴ └───────┘
typ └────┘ └─────────────────┘┴ └──────┘└─┘ └──────────┘┴┴┴┴└───────┘
doc └────┘ ┴ └─┘ └──────────┘┴ ┴ └───────┘
txt └────┘ ┴ └─┘ ┴ ┴ └───────┘
par └────┘ ┴ └─┘ ┴ ┴ └───────┘
pid ┴ ┴ └─┘ ┴ ┴ └─────┘└┘
st ──────────────────────────────────────────────────────────────────┘
162 end
st └─┘
163
164 /-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
165 cardinality of the basis. -/
166 lemma dim_eq_card_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :
id └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └─────┘ └──────┘
typ └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └─────┘ └──────┘
167 dim K V = fintype.card ι :=
id └─┘ ┴ ┴ ┴ └──────────┘ ┴
src └─┘ ┴ └──────────┘
typ └─┘ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘
168 by rw [←h.mk_range_eq_dim, cardinal.fintype_card,
id └───────────────────┘
src └───┘ └┘└───────────────────┘└─
typ └───┘└───────────────┘└┘└───────────────────┘└─
doc └───┘ └┘ └─
txt └───┘ └┘ └─
par └───┘ └┘ └─
pid └─┘ └┘ └─
st └─────────────────────┘└─────────────────────┘└─
169 set.card_range_of_injective (h.injective zero_ne_one)]
id └─────────────────────────┘ └─────────┘ └─────────┘
src ──────┘└─────────────────────────┘┴ └─────────┘┴└─────────┘└──
typ ──────┘└─────────────────────────┘┴ └─────────┘┴└─────────┘└──
doc ──────┘ ┴ ┴ └──
txt ──────┘ ┴ ┴ └──
par ──────┘ ┴ ┴ └──
pid ──────┘ ┴ ┴ └┘└
st ───────────────────────────────────────────────────────────┘┴└
170
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
171
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
172 /-- If a vector space has a finite basis, then its dimension is equal to the cardinality of the
173 basis. -/
174 lemma findim_eq_card_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :
id └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └─────┘ └──────┘
typ └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └─────┘ └──────┘
175 findim K V = fintype.card ι :=
id └────┘ ┴ ┴ ┴ └──────────┘ ┴
src └────┘ ┴ └──────────┘
typ └────┘ ┴ ┴ ┴ └──────────┘ ┴
doc └────┘ └──────────┘
176 begin
st └─────
177 haveI : finite_dimensional K V := of_finite_basis h,
id └────────────────┘ ┴ ┴ └─────────────┘ ┴
src └──────┘└────────────────┘┴ ┴ └──┘└─────────────┘┴
typ └──────┘└────────────────┘┴┴┴┴└──┘└─────────────┘┴┴
doc └──────┘└────────────────┘┴ ┴ └──┘└─────────────┘┴
txt └──────┘ ┴ ┴ └──┘ ┴
par └──────┘ ┴ ┴ └──┘ ┴
pid ┴└┘ ┴ ┴ └──┘ ┴
st ────────────────────────────────────────────────────┘└─
178 have := dim_eq_card_basis h,
id └───────────────┘ ┴
src └──────┘└───────────────┘┴
typ └──────┘└───────────────┘┴┴
doc └──────┘└───────────────┘┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ────────────────────────────┘└─
179 rw ← findim_eq_dim at this,
id └───────────┘
src └───┘└───────────┘└──────┘
typ └───┘└───────────┘└──────┘
doc └───┘└───────────┘└──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └─┘ └──────┘
st ───────────────────────────┘└─
180 exact_mod_cast this
id └──┘
src └─────────────┘ ┴
typ └─────────────┘└──┘┴
doc └─────────────┘ ┴
txt └─────────────┘ ┴
par └─────────────┘ ┴
pid ┴ ┴
st ─────────────────────┘
181 end
st └─┘
182
183 /-- If a vector space is finite-dimensional, then the cardinality of any basis is equal to its
184 `findim`. -/
185 lemma findim_eq_card_basis' [finite_dimensional K V] {ι : Type w} {b : ι → V} (h : is_basis K b) :
id └────────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src └────────────────┘ └──────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └────────────────┘ └──────┘
186 (findim K V : cardinal.{w}) = cardinal.mk ι :=
id └────┘ ┴ ┴ └──────┘ ┴ └─────────┘ ┴
src └────┘ └──────┘ ┴ └─────────┘
typ └────┘ ┴ ┴ └──────┘ ┴ └─────────┘ ┴
doc └────┘ └──────┘ └─────────┘
187 begin
st └─────
188 rcases exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
id └────────────────────┘ ┴ ┴
src └─────┘└────────────────────┘┴ ┴ └──────────────────────────┘
typ └─────┘└────────────────────┘┴┴┴┴└──────────────────────────┘
doc └─────┘ ┴ ┴ └──────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────┘
st ──────────────────────────────────────────────────────────────┘└─
189 letI: fintype s := s_finite.fintype,
id └─────┘ ┴ └──────────────┘
src └────┘└─────┘┴ └──┘└──────────────┘
typ └────┘└─────┘┴┴└──┘└──────────────┘
doc └────┘└─────┘┴ └──┘└──────────────┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid └┘ ┴ └──┘
st ────────────────────────────────────┘└─
190 have A : cardinal.mk s = fintype.card s := fintype_card _,
id └─────────┘ ┴ └──────────┘ ┴ └──────────┘
src └───────┘└─────────┘┴ ┴┴┴└──────────┘┴ └──┘└──────────┘└┘
typ └───────┘└─────────┘┴ ┴┴┴└──────────┘┴┴└──┘└──────────┘└┘
doc └───────┘└─────────┘┴ ┴ ┴└──────────┘┴ └──┘ └┘
txt └───────┘ ┴ ┴ ┴ ┴ └──┘ └┘
par └───────┘ ┴ ┴ ┴ ┴ └──┘ └┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ └──┘ └┘
st ──────────────────────────────────────────────────────────┘└─
191 have B : findim K V = fintype.card s := findim_eq_card_basis s_basis,
id └────┘ ┴ ┴ └──────────┘ ┴ └──────────────────┘ └─────┘
src └───────┘└────┘┴ ┴ ┴ ┴└──────────┘┴ └──┘└──────────────────┘┴
typ └───────┘└────┘┴┴┴┴┴ ┴└──────────┘┴┴└──┘└──────────────────┘┴└─────┘
doc └───────┘└────┘┴ ┴ ┴ ┴└──────────┘┴ └──┘└──────────────────┘┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
192 have C : cardinal.lift.{w v} (cardinal.mk ι) = cardinal.lift.{v w} (cardinal.mk s) :=
id └───────────┘ ┴ └───────────┘ └─────────┘ ┴
src └───────┘└───────────┘└─────┘ ┴ └┘ ┴└───────────┘└─────┘ └─────────┘┴ └────
typ └───────┘└───────────┘└─────┘ ┴┴└┘ ┴└───────────┘└─────┘ └─────────┘┴┴└────
doc └───────┘└───────────┘└─────┘ ┴ └┘ ┴└───────────┘└─────┘ └─────────┘┴ └────
txt └───────┘ └─────┘ ┴ └┘ ┴ └─────┘ ┴ └────
par └───────┘ └─────┘ ┴ └┘ ┴ └─────┘ ┴ └────
pid └────┘└─┘ └─────┘ ┴ └┘ ┴ └─────┘ ┴ ┴└───
st ────────────────────────────────────────────────────────────────────────────────────────
193 mk_eq_mk_of_basis h s_basis,
id └───────────────┘ ┴ └─────┘
src ───┘└───────────────┘┴ ┴
typ ───┘└───────────────┘┴┴┴└─────┘
doc ───┘└───────────────┘┴ ┴
txt ───┘ ┴ ┴
par ───┘ ┴ ┴
pid ───┘ ┴ ┴
st ──────────────────────────────┘└─
194 rw [A, ← B, lift_nat_cast] at C,
id ┴ ┴ └───────────┘
src └──┘ └──┘ └┘└───────────┘└────┘
typ └──┘┴└──┘┴└┘└───────────┘└────┘
doc └──┘ └──┘ └┘ └────┘
txt └──┘ └──┘ └┘ └────┘
par └──┘ └──┘ └┘ └────┘
pid └┘ └──┘ └┘ ┴└───┘
st ──────┘└───┘└─────────────┘┴└───┘└─
195 have : cardinal.lift.{w v} (cardinal.mk ι) = cardinal.lift.{w v} (findim K V),
id └───────────┘ └─────────┘ ┴ └───────────┘ └────┘ ┴ ┴
src └─────┘└───────────┘└─────┘ └─────────┘┴ └┘ ┴└───────────┘└─────┘ └────┘┴ ┴ ┴
typ └─────┘└───────────┘└─────┘ └─────────┘┴┴└┘ ┴└───────────┘└─────┘ └────┘┴┴┴┴┴
doc └─────┘└───────────┘└─────┘ └─────────┘┴ └┘ ┴└───────────┘└─────┘ └────┘┴ ┴ ┴
txt └─────┘ └─────┘ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴
par └─────┘ └─────┘ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴
pid └───┘└┘ └─────┘ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────┘
196 by { simp, exact C },
id ┴
src └──┘ └────┘ ┴
typ └──┘ └────┘┴┴
doc └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid ┴ ┴
st ┴└───┘└────────┘└┘└
197 exact (lift_inj.mp this).symm
id └─────────┘ └──┘
src └────┘ └─────────┘┴ └─────┘
typ └────┘ └─────────┘┴└──┘└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └───┘└┘
st ───────────────────────────────┘
198 end
st └─┘
199
200 /-- If a submodule has maximal dimension in a finite dimensional space, then it is equal to the
201 whole space. -/
202 lemma eq_top_of_findim_eq [finite_dimensional K V] {S : submodule K V}
id └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
src └────────────────┘ └───────┘
typ └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
doc └────────────────┘ └───────┘
203 (h : findim K S = findim K V) : S = ⊤ :=
id └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └────┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘ └────┘
204 begin
st └─────
205 cases exists_is_basis K S with bS hbS,
id └─────────────┘ ┴ ┴
src └────┘└─────────────┘┴ ┴ └──────────┘
typ └────┘└─────────────┘┴┴┴┴└──────────┘
doc └────┘ ┴ ┴ └──────────┘
txt └────┘ ┴ ┴ └──────────┘
par └────┘ ┴ ┴ └──────────┘
pid ┴ ┴ ┴ └──────────┘
st ──────────────────────────────────────┘└─
206 have : linear_independent K (subtype.val : (subtype.val '' bS : set V) → V),
id └────────────────┘ ┴ └─────────┘ ┴ └┘ └┘ └─┘ ┴
src └─────┘└────────────────┘┴ ┴ └─────────┘└─┘ ┴└┘┴ └─┘└─┘┴ └┘ ┴ ┴
typ └─────┘└────────────────┘┴┴┴ └─────────┘└─┘┴ ┴└┘┴└┘└─┘└─┘┴ └┘ ┴┴┴
doc └─────┘└────────────────┘┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └┘ ┴ ┴
txt └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └┘ ┴ ┴
par └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └┘ ┴ ┴
pid └───┘└┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────┘└─
207 from @linear_independent.image_subtype _ _ _ _ _ _ _ _ _
id └──────────────────────────────┘
src └───┘ └──────────────────────────────┘└──────────────────
typ └───┘ └──────────────────────────────┘└──────────────────
doc └───┘ └──────────────────
txt └───┘ └──────────────────
par └───┘ └──────────────────
pid └───┘ └──────────────────
st ─────────────────────────────────────────────────────────────
208 (submodule.subtype S) hbS.1 (by simp),
id └───────────────┘ ┴ └─┘
src ─────┘ └───────────────┘┴ └┘ └─┘ ┴└──┘┴
typ ─────┘ └───────────────┘┴┴└┘└─┘└─┘ ┴└──┘┴
doc ─────┘ ┴ └┘ └─┘ ┴└──┘┴
txt ─────┘ ┴ └┘ └─┘ ┴└──┘┴
par ─────┘ ┴ └┘ └─┘ ┴└──┘┴
pid ─────┘ ┴ └┘ └─┘ └────┘
st ────────────────────────────────────┘└───┘┴└─
209 cases exists_subset_is_basis this with b hb,
id └────────────────────┘ └──┘
src └────┘└────────────────────┘┴ └────────┘
typ └────┘└────────────────────┘┴└──┘└────────┘
doc └────┘ ┴ └────────┘
txt └────┘ ┴ └────────┘
par └────┘ ┴ └────────┘
pid ┴ ┴ └────────┘
st ────────────────────────────────────────────┘└─
210 letI : fintype b := classical.choice (finite_of_linear_independent hb.2.1),
id └─────┘ ┴ └──────────────┘ └──────────────────────────┘ └┘
src └─────┘└─────┘┴ └──┘└──────────────┘┴ └──────────────────────────┘┴ └───┘
typ └─────┘└─────┘┴┴└──┘└──────────────┘┴ └──────────────────────────┘┴└┘└───┘
doc └─────┘└─────┘┴ └──┘ ┴ ┴ └───┘
txt └─────┘ ┴ └──┘ ┴ ┴ └───┘
par └─────┘ ┴ └──┘ ┴ ┴ └───┘
pid ┴└┘ ┴ └──┘ ┴ ┴ └───┘
st ───────────────────────────────────────────────────────────────────────────┘└─
211 letI : fintype (subtype.val '' bS) := classical.choice (finite_of_linear_independent this),
id └─────┘ └─────────┘ └┘ └──────────────┘ └──────────────────────────┘ └──┘
src └─────┘└─────┘┴ └─────────┘┴ ┴ └───┘└──────────────┘┴ └──────────────────────────┘┴ ┴
typ └─────┘└─────┘┴ └─────────┘┴ ┴└┘└───┘└──────────────┘┴ └──────────────────────────┘┴└──┘┴
doc └─────┘└─────┘┴ ┴ ┴ └───┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
pid ┴└┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
212 letI : fintype bS := classical.choice (finite_of_linear_independent hbS.1),
id └─────┘ └┘ └──────────────┘ └──────────────────────────┘ └─┘
src └─────┘└─────┘┴ └──┘└──────────────┘┴ └──────────────────────────┘┴ └─┘
typ └─────┘└─────┘┴└┘└──┘└──────────────┘┴ └──────────────────────────┘┴└─┘└─┘
doc └─────┘└─────┘┴ └──┘ ┴ ┴ └─┘
txt └─────┘ ┴ └──┘ ┴ ┴ └─┘
par └─────┘ ┴ └──┘ ┴ ┴ └─┘
pid ┴└┘ ┴ └──┘ ┴ ┴ └─┘
st ───────────────────────────────────────────────────────────────────────────┘└─
213 have : subtype.val '' bS = b, from set.eq_of_subset_of_card_le hb.1
id └─────────┘ └┘ ┴ ┴ └─────────────────────────┘ └┘
src └─────┘└─────────┘┴ ┴ ┴┴┴ └───┘└─────────────────────────┘┴ └──
typ └─────┘└─────────┘┴ ┴└┘┴┴┴┴ └───┘└─────────────────────────┘┴└┘└──
doc └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └──
txt └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └──
par └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └──
pid └───┘└┘ ┴ ┴ ┴ ┴ └───┘ ┴ └──
st ─────────────────────────────┘└───────────────────────────────────────
214 (by rw [set.card_image_of_injective _ subtype.val_injective, ← findim_eq_card_basis hbS,
id └─────────────────────────┘ └───────────────────┘ └──────────────────┘ └─┘
src ───┘ ┴└──┘└─────────────────────────┘└─┘└───────────────────┘└──┘└──────────────────┘┴ └─
typ ───┘ ┴└──┘└─────────────────────────┘└─┘└───────────────────┘└──┘└──────────────────┘┴└─┘└─
doc ───┘ ┴└──┘ └─┘ └──┘└──────────────────┘┴ └─
txt ───┘ ┴└──┘ └─┘ └──┘ ┴ └─
par ───┘ ┴└──┘ └─┘ └──┘ ┴ └─
pid ───┘ └───┘ └─┘ └──┘ ┴ └─
st ──────┘└──────────────────────────────────────────────────────┘└──────────────────────────┘└─
215 ← findim_eq_card_basis hb.2, h]; apply_instance),
id └──────────────────┘ └┘ ┴
src ──────────┘└──────────────────┘┴ └──┘ ┴└┘└────────────┘┴
typ ──────────┘└──────────────────┘┴└┘└──┘┴┴└┘└────────────┘┴
doc ──────────┘└──────────────────┘┴ └──┘ ┴└┘└────────────┘┴
txt ──────────┘ ┴ └──┘ ┴└┘└────────────┘┴
par ──────────┘ ┴ └──┘ ┴└┘└────────────┘┴
pid ──────────┘ ┴ └──┘ └────────────────┘
st ─────────────────────────────────┘└───┘┴└──────────────┘┴└─
216 erw [← hb.2.2, subtype.val_range, ← this, set.set_of_mem_eq, ← subtype_eq_val, span_image],
id └┘ └───────────────┘ └──┘ └───────────────┘ └────────────┘ └────────┘
src └─────┘ └────┘└───────────────┘└──┘ └┘└───────────────┘└──┘└────────────┘└┘└────────┘┴
typ └─────┘└┘└────┘└───────────────┘└──┘└──┘└┘└───────────────┘└──┘└────────────┘└┘└────────┘┴
doc └─────┘ └────┘ └──┘ └┘ └──┘ └┘ ┴
txt └─────┘ └────┘ └──┘ └┘ └──┘ └┘ ┴
par └─────┘ └────┘ └──┘ └┘ └──┘ └┘ ┴
pid └──┘ └────┘ └──┘ └┘ └──┘ └┘ ┴
st ────────────┘└───────────────────┘└──────┘└─────────────────┘└────────────────┘└──────────┘└──
217 have := hbS.2,
id └─┘
src └──────┘ └┘
typ └──────┘└─┘└┘
doc └──────┘ └┘
txt └──────┘ └┘
par └──────┘ └┘
pid └───┘└─┘ └┘
st ──────────────┘└─
218 erw [subtype.val_range, set.set_of_mem_eq] at this,
id └───────────────┘ └───────────────┘
src └───┘└───────────────┘└┘└───────────────┘└───────┘
typ └───┘└───────────────┘└┘└───────────────┘└───────┘
doc └───┘ └┘ └───────┘
txt └───┘ └┘ └───────┘
par └───┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st ───────────────────────┘└─────────────────┘┴└──────┘└─
219 rw [this, map_top (submodule.subtype S), range_subtype],
id └──┘ └─────┘ └───────────────┘ ┴ └───────────┘
src └──┘ └┘└─────┘┴ └───────────────┘┴ └─┘└───────────┘┴
typ └──┘└──┘└┘└─────┘┴ └───────────────┘┴┴└─┘└───────────┘┴
doc └──┘ └┘ ┴ ┴ └─┘ ┴
txt └──┘ └┘ ┴ ┴ └─┘ ┴
par └──┘ └┘ ┴ ┴ └─┘ ┴
pid └┘ └┘ ┴ ┴ └─┘ ┴
st ─────────┘└─────────────────────────────┘└─────────────┘└──
220 end
st ──┘
221
222 variable (K)
223 /-- A field is one-dimensional as a vector space over itself. -/
224 @[simp] lemma findim_of_field : findim K K = 1 :=
id └────┘ ┴ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴ ┴
doc └──┘ └────┘
225 begin
st └─────
226 have := dim_of_field K,
id └──────────┘ ┴
src └──────┘└──────────┘┴
typ └──────┘└──────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ───────────────────────┘└─
227 rw [← findim_eq_dim] at this,
id └───────────┘
src └────┘└───────────┘└───────┘
typ └────┘└───────────┘└───────┘
doc └────┘└───────────┘└───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid └──┘ ┴└──────┘
st ────────────────────┘┴└──────┘└─
228 exact_mod_cast this
id └──┘
src └─────────────┘ ┴
typ └─────────────┘└──┘┴
doc └─────────────┘ ┴
txt └─────────────┘ ┴
par └─────────────┘ ┴
pid ┴ ┴
st ─────────────────────┘
229 end
st └─┘
230
231 /-- The vector space of functions on a fintype has finite dimension. -/
232 instance finite_dimensional_fintype_fun {ι : Type*} [fintype ι] :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └─────┘
233 finite_dimensional K (ι → K) :=
id └────────────────┘ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴
doc └────────────────┘
234 by { rw [finite_dimensional_iff_dim_lt_omega, dim_fun'], exact nat_lt_omega _ }
id └─────────────────────────────────┘ └──────┘ └──────────┘
src └──┘└─────────────────────────────────┘└┘└──────┘┴ └────┘└──────────┘└─┘
typ └──┘└─────────────────────────────────┘└┘└──────┘┴ └────┘└──────────┘└─┘
doc └──┘└─────────────────────────────────┘└┘ ┴ └────┘ └─┘
txt └──┘ └┘ ┴ └────┘ └─┘
par └──┘ └┘ ┴ └────┘ └─┘
pid └┘ └┘ ┴ ┴ └┘┴
st └────────────────────────────────────────┘└────────┘└──────────────────────┘└┘
235
236 /-- The vector space of functions on a fintype ι has findim equal to the cardinality of ι. -/
237 @[simp] lemma findim_fintype_fun_eq_card {ι : Type v} [fintype ι] :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └──┘ └─────┘
238 findim K (ι → K) = fintype.card ι :=
id └────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴
src └────┘ ┴ └──────────┘
typ └────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴
doc └────┘ └──────────┘
239 begin
st └─────
240 have : vector_space.dim K (ι → K) = fintype.card ι := dim_fun',
id └──────────────┘ ┴ ┴ └──────────┘ ┴ └──────┘
src └─────┘└──────────────┘┴ ┴ ┴ ┴ └┘┴┴└──────────┘┴ └──┘└──────┘
typ └─────┘└──────────────┘┴ ┴ ┴ ┴┴└┘┴┴└──────────┘┴┴└──┘└──────┘
doc └─────┘ ┴ ┴ ┴ ┴ └┘ ┴└──────────┘┴ └──┘
txt └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
par └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
st ───────────────────────────────────────────────────────────────┘└─
241 rwa [← findim_eq_dim, nat_cast_inj] at this,
id └───────────┘ └──────────┘
src └─────┘└───────────┘└┘└──────────┘└───────┘
typ └─────┘└───────────┘└┘└──────────┘└───────┘
doc └─────┘└───────────┘└┘ └───────┘
txt └─────┘ └┘ └───────┘
par └─────┘ └┘ └───────┘
pid └──┘ └┘ ┴└──────┘
st ─────────────────────┘└────────────┘┴└──────┘└─
242 end
st ──┘
243
244 /-- The vector space of functions on `fin n` has findim equal to `n`. -/
245 @[simp] lemma findim_fin_fun {n : ℕ} : findim K (fin n → K) = n :=
id ┴ └────┘ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ └────┘ └─┘ ┴
typ ┴ └────┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └──┘ └────┘
246 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
247
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
248 /-- The submodule generated by a finite set is finite-dimensional. -/
249 theorem span_of_finite {A : set V} (hA : set.finite A) : finite_dimensional K (submodule.span K A) :=
id └─┘ ┴ └────────┘ ┴ └────────────────┘ ┴ └────────────┘ ┴ ┴
src └─┘ └────────┘ └────────────────┘ └────────────┘
typ └─┘ ┴ └────────┘ ┴ └────────────────┘ ┴ └────────────┘ ┴ ┴
doc └────────┘ └────────────────┘ └────────────┘
250 is_noetherian_span_of_finite K hA
id └──────────────────────────┘ ┴ └┘
src └──────────────────────────┘
typ └──────────────────────────┘ ┴ └┘
doc └──────────────────────────┘
251
252 end finite_dimensional
253
254 namespace submodule
255 open finite_dimensional
256
257 /-- A submodule is finitely generated if and only if it is finite-dimensional -/
258 theorem fg_iff_finite_dimensional (s : submodule K V) :
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
259 s.fg ↔ finite_dimensional K s :=
id ┴└─┘ ┴ └────────────────┘ ┴ ┴
src └─┘ ┴ └────────────────┘
typ ┴└─┘ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘
260 ⟨λh, is_noetherian_of_fg_of_noetherian s h,
id ┴ └───────────────────────────────┘ ┴ ┴
src └───────────────────────────────┘
typ ┴ └───────────────────────────────┘ ┴ ┴
261 λh, by { rw ← map_subtype_top s, exact fg_map (iff_fg.1 h) }⟩
id ┴ └─────────────┘ ┴ └────┘ └────┘ ┴
src └───┘└─────────────┘┴ └────┘└────┘┴ └────┘└─┘ └┘
typ ┴ └───┘└─────────────┘┴┴ └────┘└────┘┴ └────┘└─┘┴└┘
doc └───┘└─────────────┘┴ └────┘ ┴ └────┘└─┘ └┘
txt └───┘ ┴ └────┘ ┴ └─┘ └┘
par └───┘ ┴ └────┘ ┴ └─┘ └┘
pid └─┘ ┴ ┴ ┴ └─┘ ┴┴
st └───────────────────────┘└──────────────────────────┘└┘
262
263 /-- In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding
264 quotient add up to the dimension of the space. -/
265 theorem findim_quotient_add_findim [finite_dimensional K V] (s : submodule K V) :
id └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
src └────────────────┘ └───────┘
typ └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
doc └────────────────┘ └───────┘
266 findim K s.quotient + findim K s = findim K V :=
id └────┘ ┴ ┴└───────┘ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └────┘ └───────┘ ┴ └────┘ ┴ └────┘
typ └────┘ ┴ ┴└───────┘ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └───────┘ └────┘ └────┘
267 begin
st └─────
268 have := dim_quotient_add_dim s,
id └──────────────────┘ ┴
src └──────┘└──────────────────┘┴
typ └──────┘└──────────────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ───────────────────────────────┘└─
269 rw [← findim_eq_dim, ← findim_eq_dim, ← findim_eq_dim] at this,
id └───────────┘ └───────────┘ └───────────┘
src └────┘└───────────┘└──┘└───────────┘└──┘└───────────┘└───────┘
typ └────┘└───────────┘└──┘└───────────┘└──┘└───────────┘└───────┘
doc └────┘└───────────┘└──┘└───────────┘└──┘└───────────┘└───────┘
txt └────┘ └──┘ └──┘ └───────┘
par └────┘ └──┘ └──┘ └───────┘
pid └──┘ └──┘ └──┘ ┴└──────┘
st ────────────────────┘└───────────────┘└───────────────┘┴└──────┘└─
270 exact_mod_cast this
id └──┘
src └─────────────┘ ┴
typ └─────────────┘└──┘┴
doc └─────────────┘ ┴
txt └─────────────┘ ┴
par └─────────────┘ ┴
pid ┴ ┴
st ─────────────────────┘
271 end
st └─┘
272
273 /-- The dimension of a submodule is bounded by the dimension of the ambient space. -/
274 lemma findim_le [finite_dimensional K V] (s : submodule K V) : findim K s ≤ findim K V :=
id └────────────────┘ ┴ ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └────────────────┘ └───────┘ └────┘ ┴ └────┘
typ └────────────────┘ ┴ ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └────────────────┘ └───────┘ └────┘ └────┘
275 by { rw ← s.findim_quotient_add_findim, exact nat.le_add_left _ _ }
id └─────────────┘
src └───┘ └────┘└─────────────┘└───┘
typ └───┘└──────────────────────────┘ └────┘└─────────────┘└───┘
doc └───┘ └────┘ └───┘
txt └───┘ └────┘ └───┘
par └───┘ └────┘ └───┘
pid └─┘ ┴ └──┘┴
st └──────────────────────────────────┘└──────────────────────────┘└┘
276
277 /-- The dimension of a quotient is bounded by the dimension of the ambient space. -/
278 lemma findim_quotient_le [finite_dimensional K V] (s : submodule K V) :
id └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
src └────────────────┘ └───────┘
typ └────────────────┘ ┴ ┴ └───────┘ ┴ ┴
doc └────────────────┘ └───────┘
279 findim K s.quotient ≤ findim K V :=
id └────┘ ┴ ┴└───────┘ ┴ └────┘ ┴ ┴
src └────┘ └───────┘ ┴ └────┘
typ └────┘ ┴ ┴└───────┘ ┴ └────┘ ┴ ┴
doc └────┘ └───────┘ └────┘
280 by { rw ← s.findim_quotient_add_findim, exact nat.le_add_right _ _ }
id └──────────────┘
src └───┘ └────┘└──────────────┘└───┘
typ └───┘└──────────────────────────┘ └────┘└──────────────┘└───┘
doc └───┘ └────┘ └───┘
txt └───┘ └────┘ └───┘
par └───┘ └────┘ └───┘
pid └─┘ ┴ └──┘┴
st └──────────────────────────────────┘└───────────────────────────┘└┘
281
282 end submodule
283
284 namespace linear_equiv
285 open finite_dimensional
286
287 /-- Finite dimensionality is preserved under linear equivalence. -/
288 protected theorem finite_dimensional (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :
id ┴ └─┘┴┴ └┘ └────────────────┘ ┴ ┴
src └─┘ ┴ └────────────────┘
typ ┴ └─┘┴┴ └┘ └────────────────┘ ┴ ┴
doc └─┘ ┴ └────────────────┘
289 finite_dimensional K V₂ :=
id └────────────────┘ ┴ └┘
src └────────────────┘
typ └────────────────┘ ┴ └┘
doc └────────────────┘
290 is_noetherian_of_linear_equiv f
id └───────────────────────────┘ ┴
src └───────────────────────────┘
typ └───────────────────────────┘ ┴
291
292 /-- The dimension of a finite dimensional space is preserved under linear equivalence. -/
293 theorem findim_eq (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :
id ┴ └─┘┴┴ └┘ └────────────────┘ ┴ ┴
src └─┘ ┴ └────────────────┘
typ ┴ └─┘┴┴ └┘ └────────────────┘ ┴ ┴
doc └─┘ ┴ └────────────────┘
294 findim K V = findim K V₂ :=
id └────┘ ┴ ┴ ┴ └────┘ ┴ └┘
src └────┘ ┴ └────┘
typ └────┘ ┴ ┴ ┴ └────┘ ┴ └┘
doc └────┘ └────┘
295 begin
st └─────
296 haveI : finite_dimensional K V₂ := f.finite_dimensional,
id └────────────────┘ ┴ └┘ └──────────────────┘
src └──────┘└────────────────┘┴ ┴ └──┘└──────────────────┘
typ └──────┘└────────────────┘┴┴┴└┘└──┘└──────────────────┘
doc └──────┘└────────────────┘┴ ┴ └──┘└──────────────────┘
txt └──────┘ ┴ ┴ └──┘
par └──────┘ ┴ ┴ └──┘
pid ┴└┘ ┴ ┴ └──┘
st ────────────────────────────────────────────────────────┘└─
297 rcases exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
id └────────────────────┘ ┴ ┴
src └─────┘└────────────────────┘┴ ┴ └──────────────────────────┘
typ └─────┘└────────────────────┘┴┴┴┴└──────────────────────────┘
doc └─────┘ ┴ ┴ └──────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────┘
st ──────────────────────────────────────────────────────────────┘└─
298 letI : fintype s := s_finite.fintype,
id └─────┘ ┴ └──────────────┘
src └─────┘└─────┘┴ └──┘└──────────────┘
typ └─────┘└─────┘┴┴└──┘└──────────────┘
doc └─────┘└─────┘┴ └──┘└──────────────┘
txt └─────┘ ┴ └──┘
par └─────┘ ┴ └──┘
pid ┴└┘ ┴ └──┘
st ─────────────────────────────────────┘└─
299 have A : findim K V = fintype.card s := findim_eq_card_basis s_basis,
id └────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────────────┘ └─────┘
src └───────┘└────┘┴ ┴ ┴┴┴└──────────┘┴ └──┘└──────────────────┘┴
typ └───────┘└────┘┴┴┴┴┴┴┴└──────────┘┴┴└──┘└──────────────────┘┴└─────┘
doc └───────┘└────┘┴ ┴ ┴ ┴└──────────┘┴ └──┘└──────────────────┘┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
300 have : is_basis K (λx:s, f (subtype.val x)) := f.is_basis s_basis,
id └──────┘ ┴ ┴ ┴ └─────────┘ └────────┘ └─────┘
src └─────┘└──────┘┴ ┴ └┘ └┘ ┴ └─────────┘┴ └────┘└────────┘┴
typ └─────┘└──────┘┴┴┴ └┘┴└┘┴┴ └─────────┘┴ └────┘└────────┘┴└─────┘
doc └─────┘└──────┘┴ ┴ └┘ └┘ ┴ ┴ └────┘ ┴
txt └─────┘ ┴ ┴ └┘ └┘ ┴ ┴ └────┘ ┴
par └─────┘ ┴ ┴ └┘ └┘ ┴ ┴ └────┘ ┴
pid └───┘└┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘└──┘ ┴
st ──────────────────────────────────────────────────────────────────┘└─
301 have B : findim K V₂ = fintype.card s := findim_eq_card_basis this,
id └────┘ ┴ └┘ └──────────┘ ┴ └──────────────────┘ └──┘
src └───────┘└────┘┴ ┴ ┴ ┴└──────────┘┴ └──┘└──────────────────┘┴
typ └───────┘└────┘┴┴┴└┘┴ ┴└──────────┘┴┴└──┘└──────────────────┘┴└──┘
doc └───────┘└────┘┴ ┴ ┴ ┴└──────────┘┴ └──┘└──────────────────┘┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────────────────┘└─
302 rw [A, B]
id ┴ ┴
src └──┘ └┘ └┘
typ └──┘┴└┘┴└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ──────┘└─┘┴┴
303 end
st └─┘
304
305 end linear_equiv
306
307 namespace linear_map
308 open finite_dimensional
309
310 /-- On a finite-dimensional space, an injective linear map is surjective. -/
311 lemma surjective_of_injective [finite_dimensional K V] {f : V →ₗ[K] V}
id └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
src └────────────────┘ └─┘ ┴
typ └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
doc └────────────────┘
312 (hinj : injective f) : surjective f :=
id └───────┘ ┴ └────────┘ ┴
src └───────┘ └────────┘
typ └───────┘ ┴ └────────┘ ┴
313 begin
st └─────
314 have h := dim_eq_injective _ hinj,
id └──────────────┘ └──┘
src └────────┘└──────────────┘└─┘
typ └────────┘└──────────────┘└─┘└──┘
doc └────────┘ └─┘
txt └────────┘ └─┘
par └────────┘ └─┘
pid └────┘┴└─┘ └─┘
st ──────────────────────────────────┘└─
315 rw [← findim_eq_dim, ← findim_eq_dim, nat_cast_inj] at h,
id └───────────┘ └───────────┘ └──────────┘
src └────┘└───────────┘└──┘└───────────┘└┘└──────────┘└────┘
typ └────┘└───────────┘└──┘└───────────┘└┘└──────────┘└────┘
doc └────┘└───────────┘└──┘└───────────┘└┘ └────┘
txt └────┘ └──┘ └┘ └────┘
par └────┘ └──┘ └┘ └────┘
pid └──┘ └──┘ └┘ ┴└───┘
st ────────────────────┘└───────────────┘└────────────┘┴└───┘└─
316 exact range_eq_top.1 (eq_top_of_findim_eq h.symm)
id └──────────┘ └─────────────────┘ └────┘
src └────┘└──────────┘└─┘ └─────────────────┘┴└────┘└┘
typ └────┘└──────────┘└─┘ └─────────────────┘┴└────┘└┘
doc └────┘ └─┘ └─────────────────┘┴ └┘
txt └────┘ └─┘ ┴ └┘
par └────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ───────────────────────────────────────────────────┘
317 end
st └─┘
318
319 /-- On a finite-dimensional space, a linear map is injective if and only if it is surjective. -/
320 lemma injective_iff_surjective [finite_dimensional K V] {f : V →ₗ[K] V} :
id └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
src └────────────────┘ └─┘ ┴
typ └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
doc └────────────────┘
321 injective f ↔ surjective f :=
id └───────┘ ┴ ┴ └────────┘ ┴
src └───────┘ ┴ └────────┘
typ └───────┘ ┴ ┴ └────────┘ ┴
322 ⟨surjective_of_injective,
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
doc └─────────────────────┘
323 λ hsurj, let ⟨g, hg⟩ := exists_right_inverse_linear_map_of_surjective
id └───┘ └─┘ ┴ └───────────────────────────────────────────┘
src └───────────────────────────────────────────┘
typ └───┘ └─┘ ┴ └───────────────────────────────────────────┘
324 (range_eq_top.2 hsurj) in
id └──────────┘┴ └───┘
src └──────────┘┴
typ └──────────┘┴ └───┘
325 have function.right_inverse g f,
id └────────────────────┘ ┴
src └────────────────────┘
typ └────────────────────┘ ┴
326 from λ x, show (linear_map.comp f g) x = (@linear_map.id K V _ _ _ : V → V) x, by rw hg,
id ┴ └─────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └┘
src └─────────────┘ ┴ └───────────┘ └─┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘└┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └────┘
327 injective_of_has_left_inverse ⟨g, left_inverse_of_surjective_of_right_inverse
id └───────────────────────────┘ └─────────────────────────────────────────┘
src └───────────────────────────┘ └─────────────────────────────────────────┘
typ └───────────────────────────┘ └─────────────────────────────────────────┘
328 (surjective_of_injective (injective_of_has_left_inverse ⟨_, this⟩))
id └─────────────────────┘ └───────────────────────────┘ └──┘
src └─────────────────────┘ └───────────────────────────┘
typ └─────────────────────┘ └───────────────────────────┘ └──┘
doc └─────────────────────┘
329 this⟩⟩
id └──┘
typ └──┘
330
331 lemma ker_eq_bot_iff_range_eq_top [finite_dimensional K V] {f : V →ₗ[K] V} :
id └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
src └────────────────┘ └─┘ ┴
typ └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
doc └────────────────┘
332 f.ker = ⊥ ↔ f.range = ⊤ :=
id ┴└──┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴
src └──┘ ┴ ┴ ┴ └────┘ ┴ ┴
typ ┴└──┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴
doc └──┘ └────┘
333 by rw [range_eq_top, ker_eq_bot, injective_iff_surjective]
id └──────────┘ └────────┘ └──────────────────────┘
src └──┘└──────────┘└┘└────────┘└┘└──────────────────────┘└─
typ └──┘└──────────┘└┘└────────┘└┘└──────────────────────┘└─
doc └──┘ └┘ └┘└──────────────────────┘└─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └───────────────┘└──────────┘└────────────────────────┘┴└
334
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
335 /-- In a finite-dimensional space, if linear maps are inverse to each other on one side then they
336 are also inverse to each other on the other side. -/
337 lemma mul_eq_one_of_mul_eq_one [finite_dimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) :
id └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └─┘ ┴ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
338 g * f = 1 :=
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
339 have ginj : injective g, from injective_of_has_left_inverse
id └───────┘ ┴ └───────────────────────────┘
src └───────┘ └───────────────────────────┘
typ └───────┘ ┴ └───────────────────────────┘
340 ⟨f, λ x, show (f * g) x = (1 : V →ₗ[K] V) x, by rw hfg; refl⟩,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └─┘
src ┴ ┴ └─┘ ┴ └─┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ └─┘└─┘ └──┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
pid ┴
st └───────────┘
341 let ⟨i, hi⟩ := exists_right_inverse_linear_map_of_surjective
id └─┘ ┴ └┘ └───────────────────────────────────────────┘
src └───────────────────────────────────────────┘
typ └─┘ ┴ └┘ └───────────────────────────────────────────┘
342 (range_eq_top.2 (injective_iff_surjective.1 ginj)) in
id └──────────┘┴ └──────────────────────┘┴ └──┘
src └──────────┘┴ └──────────────────────┘┴
typ └──────────┘┴ └──────────────────────┘┴ └──┘
doc └──────────────────────┘
343 have f * (g * i) = f * 1, from congr_arg _ hi,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
src ┴ ┴ ┴ ┴ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
344 by rw [← mul_assoc, hfg, one_mul, mul_one] at this; rwa ← this
id └───────┘ └─┘ └─────┘ └─────┘ └──┘
src └────┘└───────┘└┘ └┘└─────┘└┘└─────┘└───────┘ └────┘ └
typ └────┘└───────┘└┘└─┘└┘└─────┘└┘└─────┘└───────┘ └────┘└──┘└
doc └────┘ └┘ └┘ └┘ └───────┘ └────┘ └
txt └────┘ └┘ └┘ └┘ └───────┘ └────┘ └
par └────┘ └┘ └┘ └┘ └───────┘ └────┘ └
pid └──┘ └┘ └┘ └┘ ┴└──────┘ └─┘ └
st └──────────────┘└───┘└───────┘└───────┘┴└────────────────────
345
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
346 /-- In a finite-dimensional space, linear maps are inverse to each other on one side if and only if
347 they are inverse to each other on the other side. -/
348 lemma mul_eq_one_comm [finite_dimensional K V] {f g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1 :=
id └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
349 ⟨mul_eq_one_of_mul_eq_one, mul_eq_one_of_mul_eq_one⟩
id └──────────────────────┘ └──────────────────────┘
src └──────────────────────┘ └──────────────────────┘
typ └──────────────────────┘ └──────────────────────┘
doc └──────────────────────┘ └──────────────────────┘
350
351 /-- In a finite-dimensional space, linear maps are inverse to each other on one side if and only if
352 they are inverse to each other on the other side. -/
353 lemma comp_eq_id_comm [finite_dimensional K V] {f g : V →ₗ[K] V} : f.comp g = id ↔ g.comp f = id :=
id └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴└───┘ ┴ ┴ └┘ ┴ ┴└───┘ ┴ ┴ └┘
src └────────────────┘ └─┘ ┴ └───┘ ┴ └┘ ┴ └───┘ ┴ └┘
typ └────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴└───┘ ┴ ┴ └┘ ┴ ┴└───┘ ┴ ┴ └┘
doc └────────────────┘
354 mul_eq_one_comm
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
355
356 /-- The image under an onto linear map of a finite-dimensional space is also finite-dimensional. -/
357 lemma finite_dimensional_of_surjective [h : finite_dimensional K V]
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
doc └────────────────┘
358 (f : V →ₗ[K] V₂) (hf : f.range = ⊤) : finite_dimensional K V₂ :=
id ┴ └─┘┴┴ └┘ ┴└────┘ ┴ ┴ └────────────────┘ ┴ └┘
src └─┘ ┴ └────┘ ┴ ┴ └────────────────┘
typ ┴ └─┘┴┴ └┘ ┴└────┘ ┴ ┴ └────────────────┘ ┴ └┘
doc └────┘ └────────────────┘
359 is_noetherian_of_surjective V f hf
id └─────────────────────────┘ ┴ ┴ └┘
src └─────────────────────────┘
typ └─────────────────────────┘ ┴ ┴ └┘
360
361 /-- The range of a linear map defined on a finite-dimensional space is also finite-dimensional. -/
362 instance finite_dimensional_range [h : finite_dimensional K V] (f : V →ₗ[K] V₂) :
id └────────────────┘ ┴ ┴ ┴ └─┘┴┴ └┘
src └────────────────┘ └─┘ ┴
typ └────────────────┘ ┴ ┴ ┴ └─┘┴┴ └┘
doc └────────────────┘
363 finite_dimensional K f.range :=
id └────────────────┘ ┴ ┴└────┘
src └────────────────┘ └────┘
typ └────────────────┘ ┴ ┴└────┘
doc └────────────────┘ └────┘
364 f.quot_ker_equiv_range.finite_dimensional
id ┴└───────────────────┘└─────────────────┘
src └───────────────────┘└─────────────────┘
typ ┴└───────────────────┘└─────────────────┘
doc └───────────────────┘└─────────────────┘
365
366 /-- rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to
367 the dimension of the source space. -/
368 theorem findim_range_add_findim_ker [finite_dimensional K V] (f : V →ₗ[K] V₂) :
id └────────────────┘ ┴ ┴ ┴ └─┘┴┴ └┘
src └────────────────┘ └─┘ ┴
typ └────────────────┘ ┴ ┴ ┴ └─┘┴┴ └┘
doc └────────────────┘
369 findim K f.range + findim K f.ker = findim K V :=
id └────┘ ┴ ┴└────┘ ┴ └────┘ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
src └────┘ └────┘ ┴ └────┘ └──┘ ┴ └────┘
typ └────┘ ┴ ┴└────┘ ┴ └────┘ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
doc └────┘ └────┘ └────┘ └──┘ └────┘
370 by { rw [← f.quot_ker_equiv_range.findim_eq], exact submodule.findim_quotient_add_findim _ }
id └──────────────────────────────────┘
src └────┘ ┴ └────┘└──────────────────────────────────┘└─┘
typ └────┘└──────────────────────────────┘┴ └────┘└──────────────────────────────────┘└─┘
doc └────┘ ┴ └────┘└──────────────────────────────────┘└─┘
txt └────┘ ┴ └────┘ └─┘
par └────┘ ┴ └────┘ └─┘
pid └──┘ ┴ ┴ └┘┴
st └───────────────────────────────────────┘└──────────────────────────────────────────────┘└┘
371
372 end linear_map